home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Language/OS - Multiplatform Resource Library
/
LANGUAGE OS.iso
/
quintus
/
quintus0.lha
/
work
/
interp_2.06.0
< prev
next >
Wrap
Text File
|
1992-04-03
|
19KB
|
674 lines
%%% INTERPRETER
%%% version 2.00.0 (based on interp_19.1)
%%% added equality transformation
%%% version 2.00.1
%%% added equality rewriting
%%% version 2.00.4
%%% fixed input clause count when transforming equation
%%% version 2.00.6
%%% added user specified rewrite rules and orderings
%%% added "include_original_clause"
%%% version 2.01.1
%%% fixed transivity bug when asserting rewrite order
%%% version 2.01.3
%%% moved rewriting of input clauses to interpret
%%% added code to orient equations
%%% version 2.01.4
%%% modified rewriting of equations according to David Plaisted's method
%%% version 2.01.7
%%% oriented input equations literal in each direction
%%% version 2.01.9
%%% optimized term rewriting
%%% version 2.02.1
%%% added partial rewrite count
%%% version 2.03.0
%%% moved rewrite rule simplification to hyper-linking
%%% version 2.03.4
%%% printed axioms
%%% version 2.03.8
%%% rewrite clauses in round 0 when necessary
%%% version 2.04.5
%%% don't include original equations in both directions
%%% version 2.05.1
%%% added clause splitting
%%% version 2.05.3
%%% added support for Quintus Prolog
%%% version 2.05.4
%%% don't assert duplicate input clauses including pulled out forms
%%% version 2.05.8
%%% renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
%%% added priority_bound_increment
%%% version 2.06.0
%%% added bug fixes from Shie-Jue
%%%
%%% This is an interpreter to
%%% 1. read the input clauses
%%% 2. transform the input clauses into internal clause format
%%% 3. read in the commaneds in the input file and execute them
%%% 4. set supported information for clauses
%%% 5. Initialize distances
%%%
%%% Interp fails in the following cases:
%%% Read erroneous commands
%%% No user support clauses if user support strategy is specified.
%%%
%%% For axioms:
%%% axiom_list(sprfn|clause)
%%% For replace rules:
%%% replace_list
%%% For weights:
%%% weight_list
%%% For set of support:
%%% set_of_support.
%%%
%%% There are 6 errors that make this procedure fail.
%%% too_many_input_variables
%%% no_unit_clauses_with_oorr_support
%%% no_user_clauses_with_uorn_support
%%% no_neg_clauses_with_n_support
%%% error in user_rewrite section
%%% format_error_input_file
%%%
%%% Separate replace rules into two sets.
%%% repeated_replace_rules.
%%% rules.
%%% end.
%%% once_replace_rules.
%%% rules.
%%% end.
%%%
%%% Add context literals.
%%% The input replace rule is C,F,X.
%%%
interp :- not(not(interp_fail)).
interp_fail :-
cputime(TT1),
file_name(File),
seeing(Input),
see(File), !,
abolish(neg_clause_with_n_support,0),
!, interp_0(Input),
seen,
see(Input),
cputime(TT2),
TT3 is TT2 - TT1,
nl,
write_line(5,'interp(s): ',TT3), !.
interp_0(Input) :-
interp_1, !.
%%% If interp fail abnormally, close the file and return to the
%%% original input stream.
interp_0(Input) :-
seen,
see(Input), !, fail.
%%% Read until end_of_input.
interp_1 :-
read(Term),
Term \== end_of_input, !,
interp_1(Term), !,
interp_1.
%%% Provide support information.
interp_1 :-
set_priority_bound_increment_default,
process_supportset,
split_clauses.
%%% Call different procedures according to the input commands.
interp_1(axiom_list(Type)) :-
!, read_axioms(0,Type), !.
interp_1(weight_list) :-
!, interp_1_weight, !.
interp_1(repeated_replace_rules(X)) :-
!, interp_1_replace(X,u), !.
interp_1(once_replace_rules(X)) :-
!, interp_1_replace(X,o), !.
interp_1(set_of_support) :-
!, read_usersupportset.
interp_1(user_rewrite) :-
!, read_userrewrite.
interp_1(set(X)) :-
!, interp_1_command(set(X)), !.
interp_1(clear(X)) :-
!, interp_1_command(clear(X)), !.
interp_1(assign(X,V)) :-
!, interp_1_command(assign_cmd(X,V)), !.
interp_1(delete(X,V)) :-
!, interp_1_command(delete(X,V)), !.
interp_1(Term) :-
assert_print_error('Syntactic error in input file !'), !, fail.
%%% Ignore weight settings if not user control.
interp_1_weight :-
user_control, !,
read_weights, !.
interp_1_weight :-
read_till_end.
%%% Ignore replace settings if not user control.
interp_1_replace(X,T) :-
user_control, !,
read_replaces(X,T), !.
interp_1_replace(_,_) :-
read_till_end.
%%% read till end command.
read_till_end :-
read(X),
X \== end,
!, read_till_end.
read_till_end.
%%% Ignore commands if not user control.
interp_1_command(X) :-
user_control, !,
X, !.
interp_1_command(_).
%%% Read in input clauses.
read_axioms(N,Type) :-
read(Term),
!, read_axioms_1(Term,N,Type).
%%% Read in axioms one by one and transforms them into semi-internal form.
read_axioms_1(end,N,_) :-
assert_eq_axioms(N,N1),
assert(number_inclauses(N1)), !.
read_axioms_1(Term,N1,Type) :-
clause_format(Type,Term,Clause1), !,
not(not(read_axioms_2(Clause1))),
assert_original_clause(Clause1,N1,N3),
eq_trans(Clause1,Clause2),
generate_rewrite_rule(Clause1,_),
semi_internal_form(Clause2,C2),
assert_semi_internal_form(C2),
N2 is N3 + 1, !,
read_axioms(N2,Type).
read_axioms_2(C) :-
vars_tail(C,V),
var_list(V),
write_line(5,'axiom:'),
write_line(10,C),
!.
%%%
%%% Assert_original_clause asserts the original equation.
%%%
assert_original_clause(C,N1,N2) :-
equality_transform,
include_original_clause,
!,
orient_equation(C,C1),
semi_internal_form(C1,C2),
assert_semi_internal_form(C2),
N2 is N1+1,
!.
assert_original_clause(_,N,N).
%%% Transform an input formula into clause form.
clause_format(clause,P,P) :-
is_list(P), !.
clause_format(sprfn,Line,P) :-
\+ is_list(Line),
sprfn_to_clause(Line,P), !.
clause_format(_,_,_) :-
assert_print_error('Syntactic error in input file !'), !, fail.
%%% Transform a clause into a semi-internal form.
%%% If the number of variables in an input clause is greater than
%%% the number of constants in a specified list, then fail.
semi_internal_form(Clause,cl(CV1,CSize1,
by(Cn1,V11,V12,V1,W1))) :-
linearize_term(Clause,Cn1,V11,V12),
vars_tail(Clause,V1),
!,
check_input_numbervars(V1),
clause_size(Clause,CSize1),
vars_literals(Clause,W1),
compute_V_lits(W1,0,CV1).
check_input_numbervars(V1) :-
check_numbervars(V1,'Number of variables overflows in input clauses !'), !.
check_input_numbervars(V1) :-
assert_print_error('too_many_input_variables'), !, fail.
%%% Assert clause in semi internal form checking for duplicates.
assert_semi_internal_form(cl(_,CSize1,by(Cn1,V11,V11,V,_))) :-
not(not(assert_semi_internal_form_1(CSize,Cn1,V))),
!.
assert_semi_internal_form(C) :-
assertz(sent_C(C)),
!.
assert_semi_internal_form_1(CSize1,Cn1,V) :-
const_list(V),
sent_C(cl(_,CSize1,by(Cn1,V11,V11,V,_))),
!.
%%% Compute a list of variables for each literal.
vars_literals([L|Ls],[W|Ws]) :-
vars_tail(L,W), !,
vars_literals(Ls,Ws).
vars_literals([],[]).
%%% Read in weights and assert into database.
read_weights :-
read(Term),
read_weights_1(Term).
read_weights_1(end) :- !.
read_weights_1((Type,Term,W)) :-
L =.. [Type,Term,W],
assertz(L), !,
read_weights.
%%% Read in replace rules and assert into database.
read_replaces(X,T) :-
read(Term), !,
read_replaces_1(Term,X,T).
read_replaces_1(end,_,_) :- !.
read_replaces_1((C,F,X),Type,T12) :-
read_replaces_1_2(C,F,X,Type,T12),
!, read_replaces(Type,T12).
read_replaces_1((C,F),Type,T12) :-
read_replaces_1_2(C,F,[],Type,T12),
!, read_replaces(Type,T12).
read_replaces_1_2(C,F,X,Type,T12) :-
clause_format(Type,C,Clause), !,
vars_tail(Clause,V1),
!,
check_input_numbervars(V1),
vars_literals(Clause,W1),
list_multi_Ns(Clause,0,F,1,Flags),
list_multi_Ns(Clause,0,X,1,Contexts),
read_replaces_1_1(T12,Clause,V1,W1,Flags,Contexts).
read_replaces_1_1(u,Clause,V1,W1,Flags,Contexts) :-
assertz(replace_rule_1(Clause,V1,W1,Flags,Contexts)), !.
read_replaces_1_1(o,Clause,V1,W1,Flags,Contexts) :-
assertz(replace_rule_2(Clause,V1,W1,Flags,Contexts)), !.
%%% 1. Read in user support sets.
%%% 2. delete any duplicates.
%%% 3. sort the list.
%%% 4. renumber support set if equality_transform and include_original_clause
%%% 4. assert it into database.
read_usersupportset :-
read_usersupportset(S1),
delete_all_duplicates(S1,S2),
sort(S2,S3),
renumber_supportset(S3,S4),
assert(user_supportset(S4)).
read_usersupportset(U) :-
read(N), !,
read_usersupportset_1(N,U).
read_usersupportset_1(end,[]) :- !.
read_usersupportset_1(N1,[N1|U]) :-
read_usersupportset(U).
renumber_supportset(S1,S2) :-
equality_transform,
include_original_clause,
!,
renumber_supportset_1(S1,S2).
renumber_supportset(S,S).
renumber_supportset_1([],[]).
renumber_supportset_1([N1|S1],[N2,N3|S2]) :-
N3 is N1*2,
N2 is N3-1,
!,
renumber_supportset_1(S1,S2).
%%% Process support strategies and provide support informations.
process_supportset :-
support_list(User),
check_supplist(User),
!,
support_info.
%%% Transform user defined support specs into internal support form.
check_supplist(User) :-
name_list(User,Name),
legal_supplist(Name),
transf_supplist(Name,Int),
abolish(support_list_internal,1),
assert(support_list_internal(Int)), !.
check_supplist(User) :-
assert_print_error('Syntactic error in input file !'), !, fail.
%%% Transform an atom to a list of integers.
name_list([U|Us],[N|Ns]) :-
name(U,N), !,
name_list(Us,Ns).
name_list([],[]).
%%% Check if the support strategies specified are legal.
legal_supplist([N|Ns]) :-
legal_suppitem(N), !,
legal_supplist(Ns).
legal_supplist([]).
legal_suppitem([T|Ts]) :-
content_suppvalue([T]), !,
legal_suppitem(Ts).
legal_suppitem([]).
%%% Specify legal support strategies.
content_suppvalue("u").
content_suppvalue("b").
content_suppvalue("f").
content_suppvalue("r").
content_suppvalue("n").
content_suppvalue("o").
transf_supplist([N|Ns],[sup(U,B,F,R)|Is]) :-
transf_suppitem(N,U,B,F,R), !,
transf_supplist(Ns,Is).
transf_supplist([],[]).
transf_suppitem([N|Ns],U,B,F,R) :-
transf_suppvalue([N],U,B,F,R), !,
transf_suppitem(Ns,U,B,F,R).
%%% If a support is not specified, set it 0.
transf_suppitem([],U,B,F,R) :-
var_then_N(U,0),
var_then_N(B,0),
var_then_N(F,0),
var_then_N(R,0).
%%% If user support, specify what kind of user support.
%%% This information is provided for supervsior to decide the completeness
%%% of a support strategy.
transf_suppvalue("u",1,B,F,R) :- assert_once(user_support(u)).
transf_suppvalue("n",1,B,F,R) :- assert_once(user_support(n)).
transf_suppvalue("o",1,B,F,R) :- assert_once(user_support(o)).
transf_suppvalue("b",U,1,F,R).
transf_suppvalue("f",U,B,1,R).
transf_suppvalue("r",U,B,F,1).
var_then_N(N,N) :- !.
var_then_N(_,_).
%%% SET UP SUPPORT STATUS
%%%
%%% set up support environment.
%%% Set proper values in the fields of SP,and DS.
support_info :-
support_list_internal(W),
!,
support_info_1(W).
%%% If user support is given, provide user support information for clauses.
support_info_1(W) :-
specified_URsupport(W),
!, check_unit_clauses_or,
!, support_info_1_1(W).
support_info_1(W) :-
!, support_info_1_1(W).
support_info_1_1(W) :-
specified_usersupport(W),
!,
support_info_2, !.
support_info_1_1(_) :-
ubfsupp_1.
%%% If user support other than o is specified, but no user support clauses
%%% are given, then fail.
%%% If user support is o and there is no unit clause, then fail.
support_info_2 :-
user_support(o),
!, check_unit_clauses_or,
ubfsupp_o, !.
support_info_2 :-
check_uorn_support(U),
ubfsupp(1,U), !.
check_unit_clauses_or :-
sent_C(cl(_,_,by([_],_,_,_,_))), !.
check_unit_clauses_or :-
assert_print_error('No unit clauses !'), !, fail.
check_uorn_support([U|Us]) :-
user_supportset([U|Us]), !.
check_uorn_support(_) :-
assert_print_error('No user support set !'), !, fail.
specified_URsupport([sup(_,_,_,1)|Rs]).
specified_URsupport([_|Rs]) :-
!,
specified_URsupport(Rs).
specified_usersupport([sup(1,_,_,_)|Rs]).
specified_usersupport([_|Rs]) :-
!,
specified_usersupport(Rs).
%%% For all unit clauses as user support clauses.
ubfsupp_o :-
retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
ubfsupp_o_1(Cn1,V11,V12,V1,W1,CN1,CSize1),
fail.
ubfsupp_o :-
ubfsupp_1.
ubfsupp_o_1([Ln1],V11,V12,V1,W1,CN1,CSize1) :-
supplement_clause(1,CN1,CSize1,[Ln1],V11,V12,V1,W1), !.
ubfsupp_o_1(Cn1,V11,V12,V1,W1,CN1,CSize1) :-
supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
%%% Calculate support information, priorities.
supplement_clause(T,CN1,CSize1,Cn1,V11,V12,V1,W1) :-
set_sr_status(T,Cn1,CS1,CR1),
calculate_priority_clause(Cn1,CS1,CR1,CP1),
list_of_Ns(Cn1,0,F1),
assertz(sent_c(cl(CSize1,CN1,by(Cn1,V11,V12,V1,W1),
1,CS1,CR1,0,F1,CP1))).
%%% If the input clause is a user support clause.
ubfsupp(N,[N|Ns]) :-
retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1),
N2 is N + 1, !,
ubfsupp(N2,Ns).
%%% If the input clause is not a user support clause.
ubfsupp(N1,[N|Ns]) :-
retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1),
N2 is N1 + 1, !,
ubfsupp(N2,[N|Ns]).
ubfsupp(_,[]) :-
check_n_support,
ubfsupp_1.
%%% If u is specified as user support.
ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
user_support(u),
supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
%%% If n is specified as user support.
ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
negclause(Cn1),
assert_once('neg_clause_with_n_support'),
supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1).
check_n_support :-
user_support(n),
!, check_n_support_1, !.
check_n_support.
check_n_support_1 :-
neg_clause_with_n_support, !.
check_n_support_1 :-
assert_print_error('No negative clauses !'), !, fail.
%%% For backward or forward support strategies.
ubfsupp_1 :-
ubfsupp_2,
sentc_to_sentC_z.
%%% Take care of one clause at a time.
ubfsupp_2 :-
retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1),
!,
ubfsupp_2.
ubfsupp_2.
%%% Calculate support informations.
%%% The clause is in user support set.
set_sr_status(1,Cn1,sp(1,1,0),ds(0,0,1)) :-
negclause(Cn1), !.
set_sr_status(1,Cn1,sp(1,0,1),ds(0,1,0)) :-
posclause(Cn1), !.
set_sr_status(1,Cn1,sp(1,0,0),ds(0,1,1)).
%%% The clause is not in user support set.
set_sr_status(0,Cn1,sp(0,1,0),ds(X,0,1)) :-
negclause(Cn1),
infinity(X), !.
set_sr_status(0,Cn1,sp(0,0,1),ds(X,1,0)) :-
posclause(Cn1),
infinity(X), !.
set_sr_status(0,Cn1,sp(0,0,0),ds(X,1,1)) :-
infinity(X).
%%% Read user_rewrite section.
read_userrewrite :-
read(T),
read_userrewrite(T,E,O),
assert_rewrite_equiv_list(E),
assert_rewrite_order_list(O).
read_userrewrite(end,[],[]).
read_userrewrite((S->T),E,O) :-
!,
assert_rewrite_rule(1,(S->T),_),
read(T),
!,
read_userrewrite(T,E,O).
read_userrewrite(S1=S2,[S1=S2|E],O) :-
!,
read(T),
!,
read_userrewrite(T,E,O).
read_userrewrite(S1>S2,E,[S1>S2|O]) :-
!,
read(T),
!,
read_userrewrite(T,E,O).
read_userrewrite(T,_,_) :-
assert_print_error('Unrecognized expression in user_rewrite section'),
write_line(15,T),
!,
fail.
%%% Assert the constant/function/predicate symbol equivalences.
assert_rewrite_equiv_list([]).
assert_rewrite_equiv_list([S1=S2|E]) :-
assert_rewrite_equiv(S1,S2),
!,
assert_rewrite_equiv_list(E).
assert_rewrite_equiv(S1,S2) :-
parse_symbol(S1,S1a,N1),
parse_symbol(S2,S2a,N2),
not(rwe([S1a,N1,S2a,N2])),
!,
assert_rewrite_equiv_1(S1a,N1,S2a,N2).
assert_rewrite_equiv(_,_).
assert_rewrite_equiv_1(S1,N1,S2,N2) :-
not(rwo([S1,N1,S2,N2])),
not(rwo([S2,N2,S1,N1])),
!,
assert(rwe([S1,N1,S2,N2])),
assert(rwe([S2,N2,S1,N1])),
bagof1([S3,N3],rwe([S1,N1,S3,N3]),Ss1),
assert_rewrite_equiv_2(S2,N2,Ss1),
bagof1([S4,N4],rwe([S4,N4,S2,N2]),Ss2),
assert_rewrite_equiv_2(S1,N1,Ss2).
assert_rewrite_equiv_1(_,_,_,_) :-
assert_print_error('user_rewrite: S1=S2 illegal with S1>S2 or S2>S1'),
!,
fail.
assert_rewrite_equiv_2(_,_,[]).
assert_rewrite_equiv_2(S1,N1,[[S2,N2]|Ss]) :-
[S1,N1]\==[S2,N2],
not(rwe([S1,N1,S2,N2])),
!,
assert(rwe([S1,N1,S2,N2])),
assert(rwe([S2,N2,S1,N1])),
!,
assert_rewrite_equiv_2(S1,N1,Ss).
assert_rewrite_equiv_2(S,N,[[_,_]|Ss]) :-
!,
assert_rewrite_equiv_2(S,N,Ss).
assert_rewrite_order_list([]).
assert_rewrite_order_list([S1>S2|E]) :-
assert_rewrite_order(S1,S2),
!,
assert_rewrite_order_list(E).
%%% Assert the constant/function/predicate symbol orderings.
assert_rewrite_order(S1,S2) :-
parse_symbol(S1,S1a,N1),
parse_symbol(S2,S2a,N2),
not(rwo([S1a,N1,S2a,N2])),
!,
assert_rewrite_order_1(S1a,N1,S2a,N2).
assert_rewrite_order(_,_).
assert_rewrite_order_1(S1,N1,S2,N2) :-
not(rwo([S2,N2,S1,N1])),
not(rwe([S1,N1,S2,N2])),
!,
bagof1([S,N],rwe([S,N,S1,N1]),Ss1a),
bagof1([S,N],rwo([S,N,S1,N1]),Ss1b),
append(Ss1a,Ss1b,Ss1),
bagof1([S,N],rwe([S2,N2,S,N]),Ss2a),
bagof1([S,N],rwe([S2,N2,S,N]),Ss2b),
append(Ss2a,Ss2b,Ss2),
assert_rewrite_order_2([[S1,N1]|Ss1],[[S2,N2]|Ss2]).
assert_rewrite_order_1(_,_,_,_) :-
assert_print_error('user_rewrite: S1>S2 illegal with S1=S2 or S2>S1'),
!,
fail.
assert_rewrite_order_2([],_).
assert_rewrite_order_2([[S,N]|Ss1],Ss2) :-
assert_rewrite_order_3(S,N,Ss2),
!,
assert_rewrite_order_2(Ss1,Ss2).
assert_rewrite_order_3(_,_,[]).
assert_rewrite_order_3(S1,N1,[[S2,N2]|Ss]) :-
not(rwo([S1,N1,S2,N2])),
!,
assert(rwo([S1,N1,S2,N2])),
!,
assert_rewrite_order_3(S1,N1,Ss).
assert_rewrite_order_3(S,N,[[_,_]|Ss]) :-
!,
assert_rewrite_order_3(S,N,Ss).
%%% Parse a constant/function/predicate symbol into symbol and arity.
%%% Constants have arity 0.
parse_symbol(S1,S2,N) :-
S1=..[S2,N],
!.
parse_symbol(S,S,0).
%%% Assert and print an error message.
assert_print_error(X) :-
assert(error(X)),
write_line(10,X).